.. SPDX-License-Identifier: GPL-2.0 or GPL-3.0
.. Copyright © 2019 Ariadne Devos

Memory model
============
This part defines some concepts used in specifications
about usage of memory. They may be used without further
explanation.

What is a capability?
---------------------
A capability is a type an object can be subject to.
It can only allow things, but never deny things.
They can be destroyed when no longer interesting
(affine typing). Under restricted conditions, they
can be created (e.g. memory allocation). They can
typically not be duplicated (otherwise: use-after-free!).

A function may borrow some capabilities from its caller,
but they typically must be released afterwards -- not
being duplicated in the process (cf. Rust).

Sequential memory
-----------------
The following capabilities are for sequential code,
concurrently modified memory may require special instructions.

:term:`read` and :term:`write` are automatically granted for
local variables.

.. glossary::

  set
    The object has a real value, not just some unrelated bytes
    lingering around from an old operation. This is intentional,
    the RAM and processor don't care.

    C11 requires objects be set before reading (with some exceptions
    for padding bits) to avoid undefined behaviour. (To find bugs,
    search for 'uninitialised variable' on the web)

  read
    Neglecting setness, the object can be :term:`peeked`. This isn't
    really a property of the object itself, but rather is about policy,
    scope and information flow.

    Heartbleed e.g. was a buffer over-read bug.

  write
    The object can be :term:`poked`. This addresses the framing problem
    [#fframing]_: instead of specifying all variables remaining equal, only
    specify those that might change.

    C e.g. is infamous for its suspectibility to buffer overruns.
    Rust keeps tracks of array sizes and performs overflow checks,
    while staying close to the metal.

.. index::
   single: ∀

Quantified capabilities: what about arrays?
-------------------------------------------
What's the capability for a range of set objects in an array?
Our capabilities are rooted in linear logic, so a first-order
linear logic seems appropriate.

Let `S` be a finite `Foldable a` and `f` a function from `a` to
linear types. Then `∀S f` is a linear type, defined as:
`(foldMap (logical-and . f) S)`. (Dependently-typed Scheme anyone?)
(This ands together all `(f a)` where `a` belongs to `S`.

(`foldMap` and `Foldable` are taken from Haskell, the latter
may be a set, a list, a vector or a tree. Finiteness is for
avoiding non-terminating types, which may give rise to
non-consistency -- any theorem can be proved with an infinite
loop [#finfinite]_.)

Therefore, ‘∀{ k | a <= k < e} C . (index a)’ is the capability
`C` applies to elements `a..e` in the array `a`.

Other combinators
-----------------

.. index:: ?

t ? C \[ \: D \]
  If `t`, a boolean logic value holds, the capability `C`,
  else the capability `D`. `D` defaults to unit (no capability).

.. index:: ^

C ^ D
  Both the capabilities `C` and `D` -- a logical and, not
  exclusive-or! 

Effects
-------
(These may or may not correspond to those of type and effect systems.)

.. glossary::

  peeked
  peek
    Reading some memory requires :term:`set` ^ :term:`read`.

  poked
  poke
    Writing to memory requires :term:`write` and produces :term:`set`.

(Example: `x += a[i]` consists of a read from `i`, `a[i]` and `x`
and a write to `x`.)

.. rubric:: footnotes

.. [#finfinite] ‘Certified Programming with Dependent Types’ (2019) by
  ‘Adam Chlipala’ at <https://adam.chlipala.net/cpdt/html/>
  (7 ‘General Recursion’)

.. [#fframing]
  :term:`write` corresponds to Frama-C's ACSL's `assigns:` clause.
  The frame problem is discussed in ‘The Frame Problem’ by ‘Murray Shanahan’,
  in ‘The Stanford Encyclopedia of Philosophy’ (2016) at
  <https://plato.stanford.edu/archives/spr2016/entries/frame-problem>.
